Traditionally, simulation has been used to verify that an original architectural specification has been properly implemented in hardware. However, these techniques have not been able to detect all the errors in the design. As a consequence, if a faulty designed chip has been already fabricated, and delivered to customers, a costly replacement may become necessary in addition to the fabrication expenses. Thus, formal hardware verification has generally been used as a complement to traditional simulation techniques to attempt to ensure that the manufactured hardware will function properly (e.g. as designed).
This formal hardware verification has typically involved either interactive theorem proving, and/or model checking, and/or automatic sequential equivalence checking between the architectural specification and the hardware implementation (i.e. to verify that they are functionally equivalent). For example, due to the large abstraction gap between the architectural specification and the hardware implementation, formal hardware verification of floating-point division and/or square root algorithmic designs (M. D. Ercegovac, 2004) has usually involved interactive theorem proving. Unfortunately, these theorem proving techniques used to perform the aforementioned formal hardware verification have exhibited various limitations. Just by way of example, the verification process through interactive theorem proving has been very time consuming, and required high expertise, and at least some, if not all, manual processing by a user.
There is thus a need for addressing these and/or other issues associated with the prior art. For example, Kaivola (R. Kaivola, 2002) presented the formal hardware verification of the floating-point division and square root units of the Intel IA-32 Pentium 4 microprocessor, using the Forte verification framework (C.-J. H, Seger, 2005), using a combination of model checking and theorem proving in higher-order logic (HOL) (M. J. C. Gordon, 1993). As another example, Russinoff (Russinoff, 1998) presented the formal hardware verification of the floating-point division and square root units of the AMD-K7 microprocessor using ACL2 theorem proving tool (M, Kauffmann, 1996).